\begin{tabbing}
$\forall$$T$:Type, $L_{1}$, $L_{2}$, $L$:$T$ List.
\\[0ex]interleaving($T$;$L_{1}$;$L_{2}$;$L$)
\\[0ex]$\Rightarrow$ (\=$\exists$$f_{1}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$), $f_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$).\+
\\[0ex]interleaving\_occurence($T$;$L_{1}$;$L_{2}$;$L$;$f_{1}$;$f_{2}$))
\-
\end{tabbing}